Termination w.r.t. Q proof of TRS/Cimetree.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 9 SCCs with 24 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAX₁(n₃(x, y, z)) -> MAX₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MAX₁(n₃(x, y, z)) -> MAX₁(z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(MAX₁(x₁)) = 2·x₁
POL(n₃(x₁, x₂, x₃)) = 1 + 2·x₃

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MIN₁(n₃(x, y, z)) -> MIN₁(y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MIN₁(n₃(x, y, z)) -> MIN₁(y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(MIN₁(x₁)) = 2·x₁
POL(n₃(x₁, x₂, x₃)) = 1 + 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(#, 0₁(x)) -> GE₂(#, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GE₂(#, 0₁(x)) -> GE₂(#, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(#) = 0
POL(0₁(x₁)) = 1 + 2·x₁
POL(GE₂(x₁, x₂)) = 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(0₁(x₁)) = 2 + 2·x₁
POL(1₁(x₁)) = 2 + 2·x₁
POL(GE₂(x₁, x₂)) = 2·x₁ + 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(BS₁(x₁)) = 2·x₁
POL(n₃(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The remaining pairs can at least be oriented weakly.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

Used ordering: Polynomial interpretation [21]:

POL(#) = 0
POL(-₂(x₁, x₂)) = 1 + 2·x₂
POL(-¹₂(x₁, x₂)) = x₂
POL(0₁(x₁)) = 2 + 2·x₁
POL(1₁(x₁)) = 1 + 2·x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(#) = 0
POL(-₂(x₁, x₂)) = x₁
POL(-¹₂(x₁, x₂)) = x₁
POL(0₁(x₁)) = 2 + x₁
POL(1₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented:

-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(x, #) -> x
0₁(#) -> #
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(#, x) -> #

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The remaining pairs can at least be oriented weakly.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

Used ordering: Polynomial interpretation [21]:

POL(#) = 0
POL(+₂(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(+¹₂(x₁, x₂)) = 2·x₂
POL(0₁(x₁)) = 2 + x₁
POL(1₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(#) = 0
POL(+₂(x₁, x₂)) = x₁ + x₂
POL(+¹₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(0₁(x₁)) = 1 + x₁
POL(1₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented:

+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
0₁(#) -> #
+₂(#, x) -> x
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, #) -> x

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(SIZE₁(x₁)) = 2·x₁
POL(n₃(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(WB₁(x₁)) = 2·x₁
POL(n₃(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.